|
数理論理学や計算機科学の型理論として知られる分野において、カインドは型コンストラクタの型、もしくはより一般的ではないが高階型演算子の型です。カインドシステムは本質的には、基本型というで表記され「型」と呼ばれる型を持っている「一階上の」単純型付きラムダ計算で、基本型とは型パラメータを必要としない任意のデータ型のカインドです。 カインドは「（データ）型の型」という紛らわしい説明がされることもありますが、むしろ実際にはアリティ指定子です。文法的には、多相型を型コンストラクタと見なすのが自然で、従って多相でない型は零項の型コンストラクタと見なせます。しかし全ての零項の型コンストラクタ、従って全ての単相的な型は、同一の最も単純なカインドすなわちを持ちます。 高階型演算子はプログラミング言語にはめったにないので、ほとんどのプログラミング言語では実際には、カインドはデータ型とパラメータ多相を実装するのに使われるコンストラクタの型を区別するために使われます。HaskellやScalaのような、プログラム的にアクセス可能な方法でパラメータ多相の情報を提供する型システムを持つ言語において、明示的もしくは暗黙的にカインドは現れます。〔Generics of a Higher Kind 〕 == 例 == * 「型」と発音されるは全てのデータ型のカインドで、零項の型コンストラクタと見ることができ、この文脈において真の型とも呼ばれます。これは通常関数型言語の関数の型を含みます。 * は単項の型コンストラクタのカインドであり、例えばリスト型のコンストラクタのカインドです。 * は（カリー化により）二項の型コンストラクタのカインドであり、例えばペア型のコンストラクタや関数の型のコンストラクタのカインドです。（混乱しないように注意しておくと、その適用の結果自身は関数の型であり、従ってカインドの型です） * は、単項の型コンストラクタから真の型へ変換する高階型演算子のカインドです。応用についてはPierce (2002) 32章を参照のこと。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「カインド (型理論)」の詳細全文を読む スポンサード リンク
|